Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → B(b(a(a(x1))))
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
B(a(a(b(x1)))) → B(a(b(x1)))
A(b(a(x1))) → A(b(b(a(a(x1)))))
A(b(a(x1))) → A(a(x1))
A(b(a(x1))) → B(a(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → B(b(a(a(x1))))
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
B(a(a(b(x1)))) → B(a(b(x1)))
A(b(a(x1))) → A(b(b(a(a(x1)))))
A(b(a(x1))) → A(a(x1))
A(b(a(x1))) → B(a(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B(a(a(b(x1)))) → B(a(b(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule B(a(a(b(x1)))) → B(a(b(x1))) at position [0] we obtained the following new rules:
B(a(a(b(a(a(b(x0))))))) → B(a(b(a(b(x0)))))
B(a(a(b(a(x0))))) → B(a(a(b(b(a(a(x0)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B(a(a(b(a(a(b(x0))))))) → B(a(b(a(b(x0)))))
B(a(a(b(a(x0))))) → B(a(a(b(b(a(a(x0)))))))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R.
Interpretation over the domain with elements from 0 to 1.B: 0
a: 0
b: 1
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:
B.0(a.0(a.1(b.0(a.0(a.1(b.0(x0))))))) → B.0(a.1(b.0(a.1(b.0(x0)))))
B.0(a.0(a.1(b.0(a.0(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.0(x0)))))))
B.0(a.0(a.1(b.0(a.0(a.1(b.1(x0))))))) → B.0(a.1(b.0(a.1(b.1(x0)))))
B.0(a.0(a.1(b.0(a.1(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.1(x0)))))))
The TRS R consists of the following rules:
a.1(b.0(a.0(x1))) → a.0(a.1(b.1(b.0(a.0(a.0(x1))))))
a.1(b.0(a.1(x1))) → a.0(a.1(b.1(b.0(a.0(a.1(x1))))))
b.0(a.0(a.1(b.1(x1)))) → b.0(a.1(b.1(x1)))
b.0(a.0(a.1(b.0(x1)))) → b.0(a.1(b.0(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ SemLabProof2
↳ QDP
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B.0(a.0(a.1(b.0(a.0(a.1(b.0(x0))))))) → B.0(a.1(b.0(a.1(b.0(x0)))))
B.0(a.0(a.1(b.0(a.0(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.0(x0)))))))
B.0(a.0(a.1(b.0(a.0(a.1(b.1(x0))))))) → B.0(a.1(b.0(a.1(b.1(x0)))))
B.0(a.0(a.1(b.0(a.1(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.1(x0)))))))
The TRS R consists of the following rules:
a.1(b.0(a.0(x1))) → a.0(a.1(b.1(b.0(a.0(a.0(x1))))))
a.1(b.0(a.1(x1))) → a.0(a.1(b.1(b.0(a.0(a.1(x1))))))
b.0(a.0(a.1(b.1(x1)))) → b.0(a.1(b.1(x1)))
b.0(a.0(a.1(b.0(x1)))) → b.0(a.1(b.0(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ SemLabProof2
↳ QDP
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B.0(a.0(a.1(b.0(a.0(a.1(b.0(x0))))))) → B.0(a.1(b.0(a.1(b.0(x0)))))
B.0(a.0(a.1(b.0(a.0(a.1(b.1(x0))))))) → B.0(a.1(b.0(a.1(b.1(x0)))))
The TRS R consists of the following rules:
a.1(b.0(a.0(x1))) → a.0(a.1(b.1(b.0(a.0(a.0(x1))))))
a.1(b.0(a.1(x1))) → a.0(a.1(b.1(b.0(a.0(a.1(x1))))))
b.0(a.0(a.1(b.1(x1)))) → b.0(a.1(b.1(x1)))
b.0(a.0(a.1(b.0(x1)))) → b.0(a.1(b.0(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
As can be seen after transforming the QDP problem by semantic labelling [33] and then some rule deleting processors, only certain labelled rules and pairs can be used.
Hence, we only have to consider all unlabelled pairs and rules (without the decreasing rules for quasi-models).
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ SemLabProof
↳ SemLabProof2
↳ QDP
↳ RFCMatchBoundsDPProof
↳ QDP
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B(a(a(b(a(a(b(x0))))))) → B(a(b(a(b(x0)))))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 4.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
B(a(a(b(a(a(b(x0))))))) → B(a(b(a(b(x0)))))
To find matches we regarded all rules of R and P:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
B(a(a(b(a(a(b(x0))))))) → B(a(b(a(b(x0)))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
382, 383, 387, 385, 386, 384, 389, 388, 392, 393, 391, 394, 390, 397, 398, 396, 399, 395, 402, 403, 401, 404, 400, 406, 405, 408, 407, 411, 412, 410, 413, 409, 415, 414, 417, 416, 418, 419, 420, 421
Node 382 is start node and node 383 is final node.
Those nodes are connect through the following edges:
- 382 to 384 labelled B_1(0)
- 383 to 383 labelled #_1(0)
- 387 to 383 labelled b_1(0)
- 387 to 388 labelled b_1(1)
- 387 to 407 labelled b_1(2)
- 387 to 400 labelled b_1(2)
- 385 to 386 labelled b_1(0)
- 385 to 390 labelled b_1(1)
- 385 to 395 labelled b_1(1)
- 386 to 387 labelled a_1(0)
- 386 to 390 labelled a_1(1)
- 386 to 395 labelled a_1(1)
- 384 to 385 labelled a_1(0)
- 384 to 395 labelled a_1(1)
- 389 to 383 labelled b_1(1)
- 389 to 388 labelled b_1(1)
- 389 to 407 labelled b_1(2)
- 389 to 400 labelled b_1(2)
- 388 to 389 labelled a_1(1)
- 388 to 390 labelled a_1(1)
- 388 to 400 labelled a_1(2)
- 388 to 407 labelled a_1(2)
- 392 to 393 labelled b_1(1)
- 392 to 388 labelled b_1(1)
- 392 to 407 labelled b_1(2)
- 392 to 405 labelled b_1(2)
- 392 to 403 labelled b_1(2)
- 392 to 414 labelled b_1(3)
- 392 to 400 labelled b_1(2)
- 392 to 416 labelled b_1(3)
- 392 to 409 labelled b_1(3)
- 392 to 404 labelled b_1(2)
- 392 to 420 labelled b_1(4)
- 393 to 394 labelled a_1(1)
- 391 to 392 labelled b_1(1)
- 394 to 383 labelled a_1(1)
- 394 to 390 labelled a_1(1)
- 394 to 389 labelled a_1(1)
- 394 to 400 labelled a_1(2), a_1(1)
- 394 to 408 labelled a_1(1)
- 394 to 407 labelled a_1(2), a_1(1)
- 394 to 401 labelled a_1(1)
- 390 to 391 labelled a_1(1)
- 397 to 398 labelled b_1(1)
- 397 to 405 labelled b_1(2)
- 397 to 388 labelled b_1(1)
- 397 to 407 labelled b_1(2)
- 397 to 400 labelled b_1(2)
- 397 to 416 labelled b_1(3)
- 397 to 409 labelled b_1(3)
- 397 to 404 labelled b_1(2)
- 397 to 420 labelled b_1(4)
- 398 to 399 labelled a_1(1)
- 396 to 397 labelled b_1(1)
- 399 to 387 labelled a_1(1)
- 399 to 390 labelled a_1(1)
- 399 to 400 labelled a_1(2)
- 399 to 407 labelled a_1(2)
- 399 to 395 labelled a_1(1)
- 399 to 396 labelled a_1(1)
- 395 to 396 labelled a_1(1)
- 402 to 403 labelled b_1(2)
- 402 to 405 labelled b_1(2)
- 402 to 414 labelled b_1(3)
- 402 to 416 labelled b_1(3)
- 402 to 407 labelled b_1(2)
- 402 to 409 labelled b_1(3)
- 402 to 420 labelled b_1(4)
- 403 to 404 labelled a_1(2)
- 403 to 390 labelled a_1(1)
- 403 to 407 labelled a_1(2)
- 403 to 409 labelled a_1(3)
- 401 to 402 labelled b_1(2)
- 401 to 397 labelled b_1(2)
- 404 to 389 labelled a_1(2)
- 404 to 390 labelled a_1(1), a_1(2)
- 404 to 400 labelled a_1(2), b_1(2)
- 404 to 383 labelled b_1(2)
- 404 to 388 labelled b_1(1)
- 404 to 408 labelled a_1(2)
- 404 to 409 labelled a_1(3)
- 404 to 407 labelled a_1(2), b_1(2)
- 400 to 401 labelled a_1(2)
- 406 to 388 labelled b_1(2)
- 406 to 407 labelled b_1(2)
- 406 to 416 labelled b_1(3)
- 406 to 409 labelled b_1(3)
- 406 to 420 labelled b_1(4)
- 405 to 406 labelled a_1(2)
- 405 to 400 labelled a_1(2)
- 405 to 409 labelled a_1(3)
- 408 to 392 labelled b_1(2)
- 407 to 408 labelled a_1(2)
- 411 to 412 labelled b_1(3)
- 411 to 409 labelled b_1(3)
- 411 to 418 labelled b_1(4)
- 411 to 416 labelled b_1(3)
- 411 to 420 labelled b_1(4)
- 412 to 413 labelled a_1(3)
- 410 to 411 labelled b_1(3)
- 410 to 392 labelled b_1(3)
- 410 to 400 labelled b_1(3)
- 410 to 397 labelled b_1(3)
- 410 to 421 labelled a_1(3)
- 410 to 409 labelled a_1(3)
- 413 to 408 labelled a_1(3)
- 413 to 400 labelled a_1(3)
- 413 to 407 labelled a_1(3)
- 413 to 401 labelled a_1(3)
- 413 to 417 labelled a_1(3)
- 409 to 410 labelled a_1(3)
- 409 to 409 labelled a_1(3)
- 415 to 407 labelled b_1(3)
- 414 to 415 labelled a_1(3)
- 414 to 409 labelled a_1(3)
- 417 to 402 labelled b_1(3)
- 416 to 417 labelled a_1(3)
- 418 to 419 labelled a_1(4)
- 419 to 402 labelled b_1(4)
- 420 to 421 labelled a_1(4)
- 420 to 409 labelled a_1(3)
- 421 to 411 labelled b_1(4)
- 421 to 392 labelled b_1(4)
- 421 to 400 labelled b_1(4)
- 421 to 397 labelled b_1(4)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
A(b(a(x1))) → A(b(b(a(a(x1)))))
A(b(a(x1))) → A(a(x1))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
A(b(a(x1))) → A(a(x1))
The remaining pairs can at least be oriented weakly.
A(b(a(x1))) → A(b(b(a(a(x1)))))
Used ordering: Polynomial Order [21,25] with Interpretation:
POL( A(x1) ) = x1
POL( a(x1) ) = max{0, -1}
POL( b(x1) ) = 1
The following usable rules [17] were oriented:
b(a(a(b(x1)))) → b(a(b(x1)))
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ RFCMatchBoundsDPProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(b(b(a(a(x1)))))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 4.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
A(b(a(x1))) → A(b(b(a(a(x1)))))
To find matches we regarded all rules of R and P:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
A(b(a(x1))) → A(b(b(a(a(x1)))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
462, 463, 465, 466, 464, 467, 470, 471, 469, 472, 468, 474, 473, 477, 478, 476, 479, 475, 481, 480, 484, 485, 483, 486, 482, 489, 490, 488, 491, 487, 493, 492, 496, 497, 495, 498, 494, 500, 499, 501, 502
Node 462 is start node and node 463 is final node.
Those nodes are connect through the following edges:
- 462 to 464 labelled A_1(0)
- 463 to 463 labelled #_1(0)
- 465 to 466 labelled b_1(0)
- 465 to 473 labelled b_1(1)
- 465 to 480 labelled b_1(2)
- 465 to 475 labelled b_1(2)
- 465 to 482 labelled b_1(2)
- 466 to 467 labelled a_1(0)
- 464 to 465 labelled b_1(0)
- 467 to 463 labelled a_1(0)
- 467 to 468 labelled a_1(1)
- 470 to 471 labelled b_1(1)
- 470 to 473 labelled b_1(1)
- 470 to 480 labelled b_1(2)
- 470 to 475 labelled b_1(2)
- 470 to 482 labelled b_1(2)
- 471 to 472 labelled a_1(1)
- 469 to 470 labelled b_1(1)
- 472 to 463 labelled a_1(1)
- 472 to 468 labelled a_1(1)
- 468 to 469 labelled a_1(1)
- 474 to 463 labelled b_1(1)
- 474 to 473 labelled b_1(1)
- 474 to 480 labelled b_1(2)
- 474 to 475 labelled b_1(2)
- 474 to 482 labelled b_1(2)
- 473 to 474 labelled a_1(1)
- 473 to 468 labelled a_1(1)
- 473 to 475 labelled a_1(2)
- 473 to 482 labelled a_1(2)
- 477 to 478 labelled b_1(2)
- 477 to 492 labelled b_1(3)
- 477 to 480 labelled b_1(2)
- 477 to 494 labelled b_1(3)
- 477 to 501 labelled b_1(4)
- 477 to 499 labelled b_1(3)
- 477 to 487 labelled b_1(3)
- 478 to 479 labelled a_1(2)
- 478 to 468 labelled a_1(1)
- 478 to 494 labelled a_1(3)
- 478 to 475 labelled a_1(2)
- 478 to 487 labelled a_1(3)
- 476 to 477 labelled b_1(2)
- 479 to 468 labelled a_1(2), a_1(1)
- 479 to 474 labelled a_1(2)
- 479 to 482 labelled a_1(2), b_1(2)
- 479 to 487 labelled a_1(3)
- 479 to 481 labelled a_1(2)
- 479 to 475 labelled a_1(2), b_1(2)
- 479 to 473 labelled b_1(2), b_1(1)
- 479 to 463 labelled b_1(2)
- 479 to 476 labelled a_1(2)
- 479 to 480 labelled b_1(2)
- 479 to 499 labelled b_1(3)
- 479 to 483 labelled a_1(2)
- 475 to 476 labelled a_1(2)
- 481 to 470 labelled b_1(2)
- 480 to 481 labelled a_1(2)
- 484 to 485 labelled b_1(2)
- 485 to 486 labelled a_1(2)
- 483 to 484 labelled b_1(2)
- 486 to 475 labelled a_1(2)
- 482 to 483 labelled a_1(2)
- 489 to 490 labelled b_1(3)
- 489 to 492 labelled b_1(3)
- 489 to 501 labelled b_1(4)
- 489 to 499 labelled b_1(3)
- 490 to 491 labelled a_1(3)
- 488 to 489 labelled b_1(3)
- 491 to 481 labelled a_1(3)
- 491 to 476 labelled a_1(3)
- 487 to 488 labelled a_1(3)
- 493 to 480 labelled b_1(3)
- 493 to 470 labelled b_1(3)
- 493 to 475 labelled b_1(3)
- 493 to 483 labelled a_1(3)
- 493 to 500 labelled a_1(3)
- 493 to 482 labelled b_1(3)
- 492 to 493 labelled a_1(3)
- 492 to 487 labelled a_1(3)
- 496 to 497 labelled b_1(3)
- 497 to 498 labelled a_1(3)
- 495 to 496 labelled b_1(3)
- 498 to 482 labelled a_1(3)
- 498 to 475 labelled a_1(3)
- 494 to 495 labelled a_1(3)
- 500 to 477 labelled b_1(3)
- 500 to 484 labelled b_1(3)
- 499 to 500 labelled a_1(3)
- 501 to 502 labelled a_1(4)
- 502 to 489 labelled b_1(4)
- 502 to 477 labelled b_1(4)
- 502 to 484 labelled b_1(4)
We have reversed the following QTRS:
The set of rules R is
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
The set Q is empty.
We have obtained the following QTRS:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
The set Q is empty.
We have obtained the following QTRS:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
Q is empty.